:- ['framework/base.pl'].

elstep(A,B,C) :- elneeded(B,C,LST), not(member(C,LST)), conscnt(A,LST).
elstep(_,D,P) :- hasproperty2(D,P,_).
teststep(A,B,C) :- elneeded(B,_,LST), member(C,LST), conscnt(A,LST). % includes visible failure
teststep(A,B,C) :- consneeded(B,LST), member(C,LST), conscnt(A,LST). % reconstruction

derstep(A,X,Y) :- elstep(A,X,Y).         % derstep(+A,+X,-Y)
derstep(A,X,Y) :- teststep(A,X,Y).
dblefroms(M,Y) :- derstep(omega,M,Y).
dblefromsc(M,Y) :- elstep(omega,M,Y).
dblefrom(X,X). dblefrom(X,Z) :- dblefroms(X,Y), dblefrom(Y,Z).  % transitive closure of dblefroms
dblefromc(X,X). dblefromc(X,Z) :- dblefromsc(X,Y), dblefromc(Y,Z).

derfrom(_,X,X).
derfrom(A,X,Z) :- dblefroms(X,Y), dblefrom(Y,Z), derstep(A,X,Y), derfrom(A,Y,Z).
derfrom1(A,Y,X) :- derfrom(A,Y,X), !.    % derfrom1(+A,+X,+Y)

derP(A,X) :- know(A,Y), dblefrom(Y,X), derfrom1(A,Y,X).

% der(omega,_) :- !.
% der(A,X) :- derP(A,X).

derfromc(_,X,X).
derfromc(A,X,Z) :- dblefromsc(X,Y), dblefromc(Y,Z), elstep(A,X,Y), derfromc(A,Y,Z).

dercnt(A,X) :- ce(X,Z), know(A,Y), dblefrom(Y,Z), derfromc(A,Y,Z), !.
dercnt(omega,_) :- !.

conscnt(_,[]) :- !.
conscnt(A,[X|LST]) :- conscnt(A,X), conscnt(A,LST), !.
conscnt(omega,_) :- !.
conscnt(A, X) :- dercnt(A, X), !.
conscnt(A,M) :- consneeded(M,MP), conscnt(A,MP).


% list-based version

%dercs(A,X,X).
%dercs(A,X,Y) :- elstep(A,X,Y)., 

%dercntall(A,CS) :- findall(M,(know(A,Y),dblefromc(Y,M),dercnt(A,M)),CL), list_to_set(CL,CS).

% this does not save any time...
%dercntall(A,CS) :- findall(M,(know(A,Y),dblefromc(Y,M)),LDBL),
%                   list_to_set(LDBL,SDBL),
%                   findall(M,(member(M,SDBL),dercnt(A,M)),CL), list_to_set(CL,CS).

it0(A,SETM) :-
  findall(M,know(A,M),LSTM),list_to_set(LSTM,SETM).

itcnt(SETM,NEWS) :-
  findall(Z,(member(X,SETM),elstepl(SETM,X,Z)),ALLZ),append(SETM,ALLZ,NEWL),list_to_set(NEWL,NEWS).

itdo(L1,L1,L1) :- !.
itdo(_,L2,L4) :- itcnt(L2,L3), itdo(L2,L3,L4).

dercntall(A,LN) :- it0(A,L0), itcnt(L0,L1), itdo(L0,L1,LN).
  


conscntl(_,[]) :- !.
conscntl(LC,[X|LST]) :- conscntl(LC,X), conscntl(LC,LST), !.
conscntl(omega,_) :- !.
conscntl(LC,X) :- ce(X,XP), member(XP,LC), !.
conscntl(LC,M) :- consneeded(M,MP), conscntl(LC,MP).


derit(LC1,LC2) :-
  findall(M,(member(X,LC1),dblefrom(X,M),derfroml1(LC1,X,M)),LSTM),append(LC1,LSTM,LC2P),list_to_set(LC2P,LC2).

elstepl(LC,B,C) :- elneeded(B,C,LST), not(member(C,LST)), conscntl(LC,LST).
elstepl(_,D,P) :- hasproperty2(D,P,_).
teststepl(LC,B,C) :- elneeded(B,_,LST), member(C,LST), conscntl(LC,LST).   % testing rules (including vis f)
teststepl(LC,B,C) :- consneeded(B,LST), member(C,LST), conscntl(LC,LST).   % reconstruction rules
derstepl(LC,X,Y) :- elstepl(LC,X,Y).
derstepl(LC,X,Y) :- teststepl(LC,X,Y).

derfroml(_,X,X).
derfroml(LC,X,Z) :- dblefroms(X,Y), dblefrom(Y,Z), derstepl(LC,X,Y), derfroml(LC,Y,Z).
derfroml1(LC,Y,X) :- derfroml(LC,Y,X), !.    % derfrom1(+A,+X,+Y)

derl(_,X,X).
derl(CL,X,Y) :- derstepl(CL,X,Z), derl(CL,Z,Y).
derlist(A,CL,Y) :- know(A,X), derl(CL,X,Y).

%derlist(A,CL,X) :- know(A,Y), dblefrom(Y,X), derfroml1(CL,Y,X).

derall(A,SETM) :- dercntall(A,CL), findall(M,derlist(A,CL,M),LSTM), list_to_set(LSTM,SETM).

%derlist(A,M) :- findall(M,der(A,M),LSTM),list_to_set(LSTM,SETM).%
